$\forall$${\it es}$:ES, $X$:AbsInterface(Top), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ prior($X$))) $\Leftarrow\!\Rightarrow$ (($\neg$($\uparrow$first($e$))) \& (($\uparrow$(pred($e$) $\in_{b}$ $X$)) $\vee$ ($\uparrow$(pred($e$) $\in_{b}$ prior($X$)))))